$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$).
\\[0ex]Trans($T$;$a$,$b$.$R$($a$,$b$))
\\[0ex]$\Rightarrow$ \{$\forall$$a$, $b$, $c$:$T$. $R$($a$,$b$) $\Rightarrow$ strict\_part($x$,$y$.$R$($x$,$y$);$b$;$c$) $\Rightarrow$ strict\_part($x$,$y$.$R$($x$,$y$);$a$;$c$)\}